Nuprl Definition : weakPrecondSendR 11,40

at src(l):
action $a(m) 
precondition P
psends [$tg,f] on link l
== ([Rpre(source(l);ds;"$a";p;P); 

== ([Rsends(ds;locl("$a");Outcome;l;"$tg" : T;[<"$tg", s,v. [(f(s,v))]>]);

== ([Rsframe(l;"$tg";[locl("$a")])]) 
latex



clarification:

weakPrecondSendR{$a,$tg}(T;p;l;ds;P;f)
== ([Rpre(source(l);ds;"$a";p;P); 

== ([Rsends(ds;locl("$a");p-outcome(p);l;"$tg" : T;[<"$tg", s,v. [(f(s,v)) / []]> / []]) / 
== ([[Rsframe(l;"$tg";[locl("$a") / []]) / []]]) 
latex


Definitions(L), Rpre(loc;ds;a;p;P), source(l), Rsends(ds;knd;T;l;dt;g), Outcome, x : v, <ab>, x.A(x), f(a), Rsframe(lnk;tag;L), [car / cdr], locl(a), "$x", []
FDL editor aliasesweakPrecondSendR

origin